(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UF)
(declare-sort S0 0)
(declare-fun v0 () S0)
(declare-fun v1 () S0)
(declare-fun v2 () S0)
(declare-fun f0 ( S0) S0)
(declare-fun p0 ( S0) Bool)
(assert (let ((e3 (f0 v2)))
(let ((e4 (f0 v0)))
(let ((e5 (f0 v1)))
(let ((e6 (p0 e5)))
(let ((e7 (p0 e3)))
(let ((e8 (= v0 v0)))
(let ((e9 (p0 e3)))
(let ((e10 (p0 e5)))
(let ((e11 (p0 v0)))
(let ((e12 (p0 e3)))
(let ((e13 (p0 v2)))
(let ((e14 (= e4 e5)))
(let ((e15 (distinct v1 v1)))
(let ((e16 (ite e11 v0 e4)))
(let ((e17 (ite e6 e4 e4)))
(let ((e18 (ite e8 e16 v2)))
(let ((e19 (ite e12 v1 v1)))
(let ((e20 (ite e15 e5 e4)))
(let ((e21 (ite e15 e3 e17)))
(let ((e22 (ite e7 e19 e4)))
(let ((e23 (ite e14 e5 v1)))
(let ((e24 (ite e9 e16 e22)))
(let ((e25 (ite e10 e17 e22)))
(let ((e26 (ite e13 e18 e18)))
(let ((e27 (p0 e20)))
(let ((e28 (distinct v0 e19)))
(let ((e29 (p0 e20)))
(let ((e30 (distinct e17 e25)))
(let ((e31 (= e23 v2)))
(let ((e32 (distinct e4 e16)))
(let ((e33 (distinct e5 v0)))
(let ((e34 (distinct e22 e25)))
(let ((e35 (p0 e19)))
(let ((e36 (= e21 e24)))
(let ((e37 (= v1 v2)))
(let ((e38 (distinct e18 e3)))
(let ((e39 (= e26 v2)))
(let ((e40 (or e36 e10)))
(let ((e41 (and e32 e15)))
(let ((e42 (=> e37 e37)))
(let ((e43 (or e29 e39)))
(let ((e44 (and e12 e30)))
(let ((e45 (= e11 e11)))
(let ((e46 (xor e41 e45)))
(let ((e47 (xor e40 e38)))
(let ((e48 (ite e42 e44 e46)))
(let ((e49 (ite e28 e13 e35)))
(let ((e50 (ite e48 e48 e43)))
(let ((e51 (and e33 e49)))
(let ((e52 (xor e8 e50)))
(let ((e53 (= e51 e51)))
(let ((e54 (= e52 e7)))
(let ((e55 (not e53)))
(let ((e56 (= e31 e9)))
(let ((e57 (= e34 e14)))
(let ((e58 (ite e27 e55 e57)))
(let ((e59 (and e56 e56)))
(let ((e60 (and e6 e54)))
(let ((e61 (and e60 e58)))
(let ((e62 (xor e59 e47)))
(let ((e63 (and e61 e62)))
e63
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
